This post intends to promote self types as a safer, simpler, and faster alternative to inductive types and dependent pattern matching at the core of programming languages.
In summary, it should go through the problems that self types try to solve, the problems that they introduce, and then a concrete solution proposed at the end, with a syntax-directed, bidirectional type system with decidable checking.
SYNTAX at the Syntax section.